(module check-modules  (lib "eopl.ss" "eopl")

  (require "drscheme-init.scm")
  (require "lang.scm")
  (require "static-data-structures.scm")
  (require "manifest.scm")
  (require "expand-type.scm")

  (require "inferrer.scm")

  (require "unifier.scm")               ; for empty-subst
  (require "renaming.scm")
  (require "subtyping.scm")


  (provide type-of-program)
 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
  ;; type-of-program : program -> expanded-type

  (define type-of-program
    (lambda (pgm)
      (cases program pgm
        (a-program (interface-defns modules imports body)

          (let
            ((the-manifest
               (module-definitions->manifest modules)))

            (for-each
              (lambda (m-defn)
                (check-module-definition! m-defn the-manifest))
              modules)
        
            (let ((tenv (initial-tenv imports the-manifest)))
              '(pretty-print
                (list 'starting-on-body 'tenv: tenv))
              (expand-type-in-tenv 
                (expand-answer (type-of body tenv (empty-subst)))
                tenv))

            )))))

  ;; (list-of sym) * (list-of module-definition) -> environment
  (define initial-tenv
    (lambda (imports manifest)
      (let recur ((imports imports))
        (if (null? imports)
          (empty-tenv)
          (let ((m-type
                  (module-name->maybe-binding-in-tenv
                    manifest (car imports))))
            (if (not m-type)
              (eopl:error 'initial-tenv
                "attempt to import unknown module ~s"
                (car imports))
              (extend-tenv-with-module 
                (car imports) m-type
                (recur (cdr imports)))))))))

  ;; module-body * tenv -> module-type
  (define type-of-module-body
    (lambda (m-body tenv)
      (cases module-body m-body
        (var-module-body (m-name)
          (lookup-module-name-in-tenv tenv m-name))
        (defns-module-body (defns)
          (env-module-type
            (defns-to-decls defns tenv)))
        (module-app-module-body (rator-id rand-id)
          (let ((rator-type (lookup-module-name-in-tenv tenv rator-id))
                (rand-type  (lookup-module-name-in-tenv tenv rand-id)))
            (cases module-type rator-type
              (env-module-type (type-env)
                (eopl:error 'type-of-module-body
                  "attempt to apply non-parameterized module ~s"
                  rator-id))
              (proc-module-type (param-name expected-type result-type)
                (if (not (<:-module-type 
                           ;; pull components out of rand-type as per Leroy.
                           rand-type
                           expected-type tenv))
                  (raise-bad-module-application-error expected-type
                    rand-type m-body))
                (rename-in-module-type
                  result-type param-name rand-id))
              (else (eopl:error 'type-of-module-body
                      "unknown module type ~s"
                      rator-type))
              )))
        (proc-module-body (m-name m-type m-body)
          (let ((body-type
                  (type-of-module-body m-body
                    (extend-tenv-with-module m-name m-type tenv))))
            ;; what about named interfaces??
            (proc-module-type m-name m-type body-type)))
        )))

  ;; defns-to-decls : defns * tenv -> decls

  ;; convert defns to a set of declarations for just the names defined
  ;; in defns.  Do this in the context of tenv.  The tenv is extended
  ;; at every step, so we get the correct let* scoping

  (define defns-to-decls
    (lambda (defns tenv)
      (if (null? defns)
        '()
        (cases definition (car defns)
          (val-definition (name exp)
            (let ((ty (expand-answer
                        (type-of exp tenv (empty-subst)))))
              (cons
                (val-declaration name ty)
                (defns-to-decls
                  (cdr defns)
                  (extend-tenv name ty tenv)))))
          (type-definition (name ty)
            (cons
              (type-abbrev-declaration name ty)
              (defns-to-decls 
                (cdr defns)
                (extend-tenv-with-type-abbrev name 
                  (expand-type-in-tenv ty tenv)
                  tenv))))))))

  ;; m-defn * manifest -> unspecified OR fails

  (define check-module-definition!
    (lambda (m-defn manifest)
      (cases module-definition m-defn
        (a-module-definition (m-name expected-type imports m-body)
          (let ((tenv-for-m-body
                  (initial-tenv imports manifest)))
            (let ((actual-type
                    (type-of-module-body m-body tenv-for-m-body)))
              (if (not (<:-module-type 
                         actual-type
                         expected-type 
                         manifest))
                (raise-bad-module-defn-error m-name
                  expected-type actual-type))))))))

  ;; (trace check-module-defn!)

  (define raise-bad-module-application-error
    (lambda (expected-type rand-type body)
      (eopl:error 'type-of-module-body
        "Bad module application ~s" body)))

  (define raise-bad-module-defn-error
    (lambda (m-name expected-type actual-type)
      (pretty-print 
        (list 'error-in-defn-of-module: m-name
          'expected-type: expected-type
          'actual-type: actual-type))
      (eopl:error 'type-of-module-defn)))

  )